B:Type, R:(BB). one-one(B;B;R)  (n:. one-one(B;B;rel_exp(B;R;n))) 

latex

Definitions	x:A  B(x), P & Q, x:A. B(x), s = t, P  Q, False, A, f(a), x f y, rel_exp(T;R;n), x:A. B(x), x:AB(x), b, , , P  Q, t  T, Unit, left + right, if b then t else f fi , Type, one-one(A;B;R), (i = j), , , {x:A| B(x)} , i  j , A  B, #$n, -n, n+m, n - m, a < b, Void, s ~ t, {T}, SQType(T)
Lemmas	rel exp wf, ge wf, nat properties, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int